-- David Siegel, Jonathan Coveney, HW #8

module Logic (evaluate, equiv,
              satisfy, satisfiable,
              isCNF, toCNF,
              test
              ) where

import Term
import qualified Testing
import qualified TermParser as P
import qualified Set

type Set = Set.Set

------------------------------------------------------------
-- Public method declarations
------------------------------------------------------------

-- Run test functions.
test :: IO ()

-- Given a TruthAssignment, evaluate a Term in that model.
evaluate :: TruthAssignment -> Term -> Bool

-- Alias for main satisfaction function.
satisfy :: KnowledgeBase -> Maybe TruthAssignment

-- DPLL algorithm for checking satisfiability for a set of sentences.
dpllSatisfy :: KnowledgeBase -> Maybe TruthAssignment

-- WalkSAT algorithm for checking satisfiability for a set of sentences.
walkSatisfy :: KnowledgeBase -> Maybe TruthAssignment

-- Determines whether a set of sentences is satisfiable.
satisfiable :: KnowledgeBase -> Bool

-- Whether two terms are logically equivalent.
equiv :: Term -> Term -> Bool

-- Whether a Term is in CNF.
isCNF :: Term -> Bool

-- Convert a Term to CNF.
toCNF :: Term -> Term

------------------------------------------------------------
-- Private method declarations
------------------------------------------------------------

-- Gives the following TruthAssignment in a truth table.
next :: TruthAssignment -> TruthAssignment

-- Simplifies iif and if expressions
ifElim :: Term -> Term

-- Negation elimination.
negElim :: Term -> Term

-- Distribute And over Or
distribute :: Term -> Term

-- Detects if a Term structure has an And operator in it
hasAnd :: Term -> Bool

-- Detects the literals used in a given term
literals :: Term -> Set Term

-- Detects the literal s used in a knowledgebase
allLiterals :: KnowledgeBase -> Set Term

------------------------------------------------------------
-- Public method implementations
------------------------------------------------------------

evaluate ta t =
    case t of
        Iff a b       -> evaluate ta a == evaluate ta b
        If a b        -> not (evaluate ta a) || evaluate ta b
        And a b       -> evaluate ta a && evaluate ta b
        Or a b        -> evaluate ta a || evaluate ta b
        Not a         -> not (evaluate ta a)
        FalseValue    -> False
        TrueValue     -> True
        t@(Literal a) -> case lookup t ta of
                        Just truth -> truth
                        Nothing    -> error $ "No truth assignment for \'"
                                                            ++ [a] ++ "\'"
        
satisfy = dpllSatisfy

dpllSatisfy kb =
    let kb' = map toCNF kb
        ls  = allLiterals kb'
        ta  = zip (Set.toList ls) (repeat False) in
    aux ta kb'
    where aux ta kb =
            if and $ map (evaluate ta) kb
              then Just ta
              else if and (map snd ta) -- If all are True, then we're done.
                     then Nothing
                     else aux (next ta) kb

next ta = aux ta True
            where aux ((t, val) : ta) cin =
                    (t, val /= cin) : aux ta (cin && val)
                  aux [] _                = []

walkSatisfy _ = Just []

satisfiable ts = case satisfy ts of
                    Nothing -> False
                    _       -> True

equiv t1 t2 = satisfiable [t1 `Iff` t2]

isCNF t = (not . or) $ map hasAnd (andClauses t)

toCNF = distribute . negElim . ifElim

------------------------------------------------------------
-- Private method implementations
------------------------------------------------------------
            
literals = Set.mkSet . aux
           where aux t =
                    case t of
                        Iff a b   -> aux a ++ aux b
                        If a b    -> aux a ++ aux b
                        And a b   -> aux a ++ aux b
                        Or a b    -> aux a ++ aux b
                        Not a     -> aux a
                        Literal a -> [Literal a]
                        _         -> []

allLiterals = (foldr Set.union Set.empty) . (map literals)

distribute t = if isCNF t
                   then t
                   else (toCNF . distrib) t
               where distrib t =
                      case t of
                        Or (And a b) c -> distaux c a b
                        Or a (And b c) -> distaux a b c
                        a `Or` b       -> distrib a `Or` distrib b
                        a `And` b      -> distrib a `And` distrib b
                        Not a          -> Not $ distrib a
                        Literal a      -> Literal a
                        a              -> (distrib.negElim.ifElim) a
                     distaux a b c  =
                        Or (distrib a) (distrib b)
                        `And`
                        Or (distrib a) (distrib c)

andClauses t =
    case t of
        a `And` b -> andClauses a ++ andClauses b
        a         -> [a]

ifElim t =
  case t of
    t1 `Iff` t2 -> ifElim $ If t1 t2 `And` If t2 t1
    t1 `If` t2  -> ifElim $ Not t1 `Or` t2
    And t1 t2   -> ifElim t1 `And` ifElim t2
    Or t1 t2    -> ifElim t1 `Or` ifElim t2
    Not t1      -> Not $ ifElim t1
    term        -> term

negElim t = if undist t
              then (negElim.dstrneg) t
              else t
            where undist t =
                    case t of
                      Not (a `And` b) -> True
                      Not (a `Or` b)  -> True
                      (a `Or` b)      -> undist a || undist b
                      (a `And` b)     -> undist a || undist b
                      Not (Not a)     -> True
                      t               -> False
                  dstrneg t =
                    case t of
                      Not (Not a)     -> dstrneg a
                      Not (a `And` b) -> nn a `Or` nn b
                      Not (a `Or` b)  -> nn a `And` nn b
                      Not a           -> nn a
                      a `And` b       -> dstrneg a `And` dstrneg b
                      a `Or` b        -> dstrneg a `Or` dstrneg b
                      Literal a       -> Literal a
                      e               -> (negElim.ifElim) e
                  nn = Not . dstrneg

hasAnd t =
    case t of
        a `And` b -> True
        a `Or` b  -> hasAnd a || hasAnd b
        Not a     -> hasAnd a
        a         -> False

distribtest t =
  case t of
    Or (And a b) c -> distaux c a b
    Or a (And b c) -> distaux a b c
    a `Or` b       -> distribtest a `Or` distribtest b
    a `And` b      -> distribtest a `And` distribtest b
    Not a          -> Not $ distribtest a
    Literal a      -> Literal a
    a              -> (distribtest.negElim.ifElim) a
  where distaux a b c  =
          Or (distribtest a) (distribtest b)
          `And`
          Or (distribtest a) (distribtest c)

------------------------------------------------------------
-- Tests
------------------------------------------------------------

prop_toCNF :: Term -> Bool
prop_toCNF = isCNF . toCNF

prop_distrib :: Term -> Bool
prop_distrib t = t `equiv` distribtest t

propshow :: Term->Bool
propshow t = error (show t ++ "  **  " ++ show (distribtest t `equiv` t))

prop_negElim :: Term -> Bool
prop_negElim t = t `equiv` negElim t

prop_ifElim :: Term -> Bool
prop_ifElim t = t `equiv` ifElim t

-- These do not utilize quickcheck properly, rather they make it so that
-- quickcheck will evaluate to true iff the tests evaluate to true. The test
-- cases that qc generates, however, are ignored.
prop_equiv :: Term -> Bool
prop_equiv _ = let eq s1 s2 = P.justStringToTerm s1 `equiv` P.justStringToTerm s2 in
               and ["A|B" `eq` "~~(A|B)",
                    "A <=> B" `eq` "(A=>B) & (B=>A)",
                    "A => (B|C)" `eq` "~(B|C) => ~A",
                    "~(A | B | C | D | E)" `eq` "~A & ~B & ~C & ~D & ~E",
                    "~(A & B & C & D & E)" `eq` "~A | ~B | ~C | ~D | ~E",
                    not $ "~B" `eq` "B"
                   ]

prop_satisfiable ::  Term -> Bool
prop_satisfiable _ = let sat s = satisfiable [P.justStringToTerm s] in
                     and [sat "A|B",
                          sat "A <=> B",
                          sat "A => (B|C)",
                          not $ sat "B & ~B",
                          sat "(A & B & C & D) <=> (~A & ~B & ~C & ~D)"
                         ]

prop_evaluate :: Term -> Bool
prop_evaluate _ = let ta = [(Literal 'A',True),
                            (Literal 'B',False),
                            (Literal 'C',True),
                            (Literal 'D',True),
                            (Literal 'E',False)] in
                      and $ map ((evaluate ta).(P.justStringToTerm))
                          ["A<=>C",
                           "~((B|C)<=>(D&E))",
                           "(B|E)=>C"
                          ]

prop_literals :: Term -> Term -> Bool
prop_literals t1 t2 =
  Set.union (literals t1) (literals t2) == allLiterals (t1:[t2])

test = do Testing.quickcheck prop_literals
          mapM_ Testing.quickcheck [prop_toCNF,
                                    prop_distrib,
                                    prop_negElim,
                                    prop_ifElim,
                                    prop_equiv,
                                    prop_satisfiable,
                                    prop_evaluate
                                   ]
